The present invention generally relates to the field of hardware circuit verification by means of a software circuit model. More specifically, the present invention relates to verifying the behavior of a logic level circuit model to satisfy certain specified properties.
Recent increases in the complexity of modern integrated circuits has exacerbated the difficulty of verifying design correctness. The verification phase of a typical integrated circuit design project consumes approximately 70–80% of the total time and resources dedicated to a project. Flaws in the design that are not found during the verification phase have significant economic impact in terms of increased time-to-market and reduced profit margins.
A typical integrated circuit design flow includes many steps that proceed in a sequential manner, with each step depending on the results of the previous step. Consequently, when a flaw is discovered in a step, all the previous steps must be repeated, often at a significant cost. Hence, it is highly desirable to find and fix design flaws as early as possible in a design flow.
Traditionally, simulation-based techniques have been used to verify design correctness. Transistor-level simulation based techniques were used in the early 1970s and logic gate-level simulation based techniques were used in the late 1980s. As the complexity of designs increased with the passage of time, drawbacks associated with these techniques came into light. These techniques became less effective because of their inability to completely and quickly verify large designs. A popular alternative is the use of Register Transfer Language (RTL)-level simulation. Contemporary verification and debugging tools use various levels of abstractions for defining design specifications. These abstractions are expressed in high-level description languages. High-level description languages provide a number of functionalities for analyzing and verifying a design while performing simulation. For example, a designer can navigate the design hierarchy, view the RTL source code, and set breakpoints on a statement of an RTL source code to stop the simulation. Also, line numbers are provided in the RTL source code to identify different lines and statements. Further, the verification and debugging tools often support viewing and tracing variables and some times even signal values. These RTL-level simulation tools typically also offer these and other types of RTL debugging functionalities.
The verification tools as mentioned above typically follow a design flow. In the first step of the design flow, the conceptual nature of the integrated circuit is determined. The desired functionality of a circuit is expressed as a collection of properties or specifications, and possibly as a model of the behavior in a high-level language such as C++. The RTL model of the digital circuit is built based upon knowledge of the specifications or the high-level model. The RTL model is expressed in a hardware description language (HDL) such as Verilog available from Cadence Design Systems, Inc. of Santa Clara, Calif. or VHDL available from IEEE of New York, N.Y. Many other steps such as synthesis, timing optimization, clock tree insertion, place and route, etc., yield subsequent transformations of the design. These transformations eventually result in a set of masks that are fabricated into integrated circuits. The current invention is targeted at finding design flaws in the RTL model of the design, which is a very early phase of the design flow.
In the design flow, creation of RTL source code is followed by verification so as to check the compliance of the RTL source code to the design specifications. Three approaches commonly used to verify the design at the RTL level are simulation, emulation and formal methods.
Simulation is one of the most prevalent methods used to determine whether the design is in accordance with the specifications by simulating the behavior of the RTL model. The simulation process uses RTL source code and a “Test Bench” to verify a design. The Test Bench contains a subset of all possible inputs to the circuit/logic. For an ‘n’ input circuit, there are 2n possible inputs at any given time. For large n, e.g., for a complex design, the number of possible input sequences becomes prohibitively large. To simplify this, only a subset of all possible inputs is described in any given Test Bench. An example of such a tool is Ncverilog from Cadence Design Systems, Inc. of Santa Clara, Calif. To simulate the RTL model, a Test Bench must be created that provides appropriate input stimulus to the RTL model. Creating the Test Bench is a time consuming process. The process of simulating the Test Bench is also time consuming. Furthermore, it is effectively impossible to create enough test cases to completely verify that the specified properties of the design are true. This is because of the sheer number of possible inputs, and also because it requires in-depth knowledge and tremendous creativity on the part of the Test Bench creator to imagine the worst-case scenarios.
Emulation is similar to simulation, except that the design is mapped to special purpose hardware rather than simulating the design on a general-purpose computer. Emulation is significantly faster than simulation, but shares the same problems with Test Bench generation and creating worst-case scenarios.
An increasingly popular alternative is to use formal methods to completely verify properties of a design. Formal methods use mathematical techniques to prove that a design property is either always true, or to provide an example input sequence (referred to as a counterexample) demonstrating that the property is false. Tools using formal methods to verify properties are known as Model Checkers. An example of a conventional model checking tool is the Formal Check tool from Cadence Design Systems, Inc. of Santa Clara, Calif.
FIG. 1 shows an example of a property 120 and an environmental constraint 118 that could be applied to a circuit model 100. Property 120 specifies the behavior of the output signals (OUT_0 110, OUT_1 112, PREV_OUT_0 114, PREV_OUT_1 116) Environmental constraint 118 is a Boolean expression that specifies constraint on the input signals (X_0 102, X_1 104, X_2 106).
When the conventional method is applied to verify the property of a circuit model, there are three possible outcomes: (1) The system determines that the property is true for all input sequences that satisfy the set of environmental constraints. (2) The system is unable to make a determination due to lack of computing resource (time or memory). (3) The system determines that the property is false. In the latter case, the conventional system produces a counterexample that satisfies the set of environmental constraints, but for which the property fails to be true.
Two issues inhibit the widespread use of model checking. The first is performance. Resources used to perform verification are typically exponentially related to the number of registers in the circuit model. This is referred to as the “state space explosion” problem. Many conventional Model Checkers analyze the entire design before proving a particular property. The complexity and size of modern integrated circuits, combined with the state space explosion problem, make it impossible to use such Model Checkers on large designs.
Instead of analyzing the entire design, other conventional Model Checkers analyze a portion of the design relevant to a particular property. This includes all portions of the design between the signals relevant to the property and the primary inputs. An example of a conventional system that implements this property dependent design analysis is the COSPAN model checking engine referred to in R. P. Kurshan, “Formal Verification in a Commercial Setting”, Design Automation Conference, pp. 258–262, June 1997, Anaheim, Calif. However, even the property relevant portion of the design can be very large. Thus, in this case the state space explosion problem can result in severe performance problems.
No conventional system permits complete control over the region of the circuit model to be examined when verifying a particular property. The user typically resorts to manually modifying the design by removing and replacing parts of the design in order to determine if a property is true. An example of this design surgery is described in S. G. Govindaraju et al., “Counterexample-Guided Choice of Projections in Approximate Symbolic Model Checking”, IEEE International Conference on Computer-Aided Design, pp. 115–119, November 2000. This modification of the design introduces the possibility of human error and requires additional steps.
Another issue that inhibits widespread use of model checking is usability. In the conventional systems, it is impossible to express many practical environmental constraints and properties without either modifying the design, or without a detailed knowledge of the internal details of the design. The set of environmental constraints and properties of interface protocols can be encapsulated in an additional circuit model known as a monitor. An example of a monitor may be found in K. Shimizu et al., “Monitor-Based Formal Specification of PCI”, Proceedings of the 3rd International Conference of Formal Methods in Computer-Aided Design, November 2000. This additional circuit model allows users to easily express environmental constraints and related properties. But no conventional system permits the user to connect an additional circuit model such as an interface monitor to a circuit model without modifying the design.
Hence, there is a need for a system and a method that verifies a circuit model in a short duration of time. Further, there is a need for a system and a method that permits complete control over the region of the circuit model to be examined while checking for a particular property and that does not involve any modification of the design. There is also a need for a method and a system that permits the user to connect an additional circuit model representing the environmental constraints of a circuit model without modifying the design. Also, there is a need for a system and a method that verifies the design of a circuit model without modifying the design.